ra, rt:(IdId), k:Knd. kind-rename(ra;rt;k)  Knd 

latex

Definitions	kind-rename(ra;rt;k), kindcase(k; a.f(a); l,t.g(l;t) ), x. t(x), x,y. t(x;y), locl(a), rcv(l,tg), x:A. B(x), IdLnk, Knd, t  T, Id
Lemmas	Id wf, Knd wf, IdLnk wf, rcv wf, locl wf, kindcase wf